Program Verification
   HOME

TheInfoList



OR:

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended
algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
s underlying a system with respect to a certain
formal specification In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verif ...
or property, using
formal methods In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the exp ...
of mathematics. Formal verification can be helpful in proving the correctness of systems such as:
cryptographic protocol A security protocol (cryptographic protocol or encryption protocol) is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol descr ...
s, combinational circuits, digital circuits with internal memory, and software expressed as
source code In computing, source code, or simply code, is any collection of code, with or without comments, written using a human-readable programming language, usually as plain text. The source code of a program is specially designed to facilitate the w ...
. The verification of these systems is done by providing a
formal proof In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the seq ...
on an abstract mathematical model of the system, the correspondence between the mathematical model and the nature of the system being otherwise known by construction. Examples of mathematical objects often used to model systems are:
finite-state machine A finite-state machine (FSM) or finite-state automaton (FSA, plural: ''automata''), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number o ...
s,
labelled transition system In theoretical computer science, a transition system is a concept used in the study of computation. It is used to describe the potential behavior of discrete systems. It consists of state (computer science), states and transitions between states, ...
s,
Petri net A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph that ...
s,
vector addition system A vector addition system (VAS) is one of several mathematical modeling languages for the description of distributed systems. Vector addition systems were introduced by Richard M. Karp and Raymond E. Miller in 1969, and generalized to vector addit ...
s, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as
operational semantics Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execut ...
, denotational semantics, axiomatic semantics and Hoare logic.


Approaches

One approach and formation is model checking, which consists of a systematically exhaustive exploration of the mathematical model (this is possible for finite models, but also for some infinite models where infinite sets of states can be effectively represented finitely by using abstraction or taking advantage of symmetry). Usually, this consists of exploring all states and transitions in the model, by using smart and domain-specific abstraction techniques to consider whole groups of states in a single operation and reduce computing time. Implementation techniques include state space enumeration, symbolic state space enumeration, abstract interpretation, symbolic simulation, abstraction refinement. The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL),
Property Specification Language Property Specification Language (PSL) is a temporal logic extending linear temporal logic with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of regular expressions and syntactic su ...
(PSL),
SystemVerilog SystemVerilog, standardized as IEEE 1800, is a hardware description and hardware verification language used to model, design, simulate, test and implement electronic systems. SystemVerilog is based on Verilog and some extensions, and since ...
Assertions (SVA), or computational tree logic (CTL). The great advantage of model checking is that it is often fully automatic; its primary disadvantage is that it does not in general scale to large systems; symbolic models are typically limited to a few hundred bits of state, while explicit state enumeration requires the state space being explored to be relatively small. Another approach is deductive verification. It consists of generating from the system and its specifications (and possibly other annotations) a collection of mathematical ''proof obligations'', the truth of which imply conformance of the system to its specification, and discharging these obligations using either proof assistants (interactive theorem provers) (such as HOL,
ACL2 ACL2 ("A Computational Logic for Applicative Common Lisp") is a software system consisting of a programming language, created by Timothy Still it was an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed t ...
, Isabelle,
Coq Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...
or PVS), or automatic theorem provers, including in particular
satisfiability modulo theories In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvi ...
(SMT) solvers. This approach has the disadvantage that it may require the user to understand in detail why the system works correctly, and to convey this information to the verification system, either in the form of a sequence of theorems to be proved or in the form of specifications (invariants, preconditions, postconditions) of system components (e.g. functions or procedures) and perhaps subcomponents (such as loops or data structures).


Software

Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Subareas of formal verification include deductive verification (see above), abstract interpretation,
automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ma ...
,
type system In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progr ...
s, and lightweight formal methods. A promising type-based verification approach is dependently typed programming, in which the types of functions include (at least part of) those functions' specifications, and type-checking the code establishes its correctness against those specifications. Fully featured dependently typed languages support deductive verification as a special case. Another complementary approach is program derivation, in which efficient code is produced from functional specifications by a series of correctness-preserving steps. An example of this approach is the Bird–Meertens formalism, and this approach can be seen as another form of correctness by construction. These techniques can be ''
sound In physics, sound is a vibration that propagates as an acoustic wave, through a transmission medium such as a gas, liquid or solid. In human physiology and psychology, sound is the ''reception'' of such waves and their ''perception'' b ...
'', meaning that the verified properties can be logically deduced from the semantics, or ''unsound'', meaning that there is no such guarantee. A sound technique yields a result only once it has covered the entire space of possibilities. An example of an unsound technique is one that covers only a subset of the possibilities, for instance only integers up to a certain number, and give a "good-enough" result. Techniques can also be '' decidable'', meaning that their algorithmic implementations are guaranteed to terminate with an answer, or undecidable, meaning that they may never terminate. By bounding the scope of possibilities, unsound techniques that are decidable might be able to be constructed when no decidable sound techniques are available.


Verification and validation

Verification Verify or verification may refer to: General * Verification and validation, in engineering or quality management systems, is the act of reviewing, inspecting or testing, in order to establish and document that a product, service or system meets ...
is one aspect of testing a product's fitness for purpose. Validation is the complementary aspect. Often one refers to the overall checking process as V & V. * Validation: "Are we trying to make the right thing?", i.e., is the product specified to the user's actual needs? * Verification: "Have we made what we were trying to make?", i.e., does the product conform to the specifications? The verification process consists of static/structural and dynamic/behavioral aspects. E.g., for a software product one can inspect the source code (static) and run against specific test cases (dynamic). Validation usually can be done only dynamically, i.e., the product is tested by putting it through typical and atypical usages ("Does it satisfactorily meet all
use case In software and systems engineering, the phrase use case is a polyseme with two senses: # A usage scenario for a piece of software; often used in the plural to suggest situations where a piece of software may be useful. # A potential scenario ...
s?").


Automated program repair

Program repair is performed with respect to an oracle, encompassing the desired functionality of the program which is used for validation of the generated fix. A simple example is a test-suite—the input/output pairs specify the functionality of the program. A variety of techniques are employed, most notably using
satisfiability modulo theories In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvi ...
(SMT) solvers, and
genetic programming In artificial intelligence, genetic programming (GP) is a technique of evolving programs, starting from a population of unfit (usually random) programs, fit for a particular task by applying operations analogous to natural genetic processes to t ...
, using evolutionary computing to generate and evaluate possible candidates for fixes. The former method is deterministic, while the latter is randomized. Program repair combines techniques from formal verification and
program synthesis In computer science, program synthesis is the task to construct a program that provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both fields ...
. Fault-localization techniques in formal verification are used to compute program points which might be possible bug-locations, which can be targeted by the synthesis modules. Repair systems often focus on a small pre-defined class of bugs in order to reduce the search space. Industrial use is limited owing to the computational cost of existing techniques.


Industry use

The growth in complexity of designs increases the importance of formal verification techniques in the hardware industry. At present, formal verification is used by most or all leading hardware companies, but its use in the
software industry The software industry includes businesses for development, maintenance and publication of software that are using different business models, mainly either "license/maintenance based" (on-premises) or "Cloud based" (such as SaaS, PaaS, IaaS, MBa ...
is still languishing. This could be attributed to the greater need in the hardware industry, where errors have greater commercial significance. Because of the potential subtle interactions between components, it is increasingly difficult to exercise a realistic set of possibilities by simulation. Important aspects of hardware design are amenable to automated proof methods, making formal verification easier to introduce and more productive. , several operating systems have been formally verified: NICTA's Secure Embedded L4 microkernel, sold commercially as seL4 by OK Labs; OSEK/VDX based real-time operating system ORIENTAIS by
East China Normal University East China Normal University (ECNU) is a comprehensive public research university in Shanghai, China. It was formed in 1951 by the merger of the Great China University (est. 1924) and Kwang Hua University (est. 1925) and originated from the St. ...
; Green Hills Software's Integrity operating system; and
SYSGO SYSGO GmbH is a German information technologies company that supplies operating systems and services for embedded systems with high safety and security-related requirements, using Linux. For security-critical applications, the company offers the ...
's PikeOS. In 2016, a team led by Zhong Shao at Yale developed a formally verified operating system kernel called CertiKOS. As of 2017, formal verification has been applied to the design of large computer networks through a mathematical model of the network, and as part of a new network technology category, intent-based networking. Network software vendors that offer formal verification solutions include
Cisco Cisco Systems, Inc., commonly known as Cisco, is an American-based multinational digital communications technology conglomerate corporation headquartered in San Jose, California. Cisco develops, manufactures, and sells networking hardware, ...
Forward Networks and Veriflow Systems. The SPARK programming language provides a toolset which enables software development with formal verification and is used in several high-integrity systems. The CompCert C compiler is a formally verified C compiler implementing the majority of ISO C.


See also

*
Automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ma ...
* Model checking * List of model checking tools * Formal equivalence checking * Proof checker *
Property Specification Language Property Specification Language (PSL) is a temporal logic extending linear temporal logic with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of regular expressions and syntactic su ...
* Selected formal verification bibliography *
Static code analysis In computer science, static program analysis (or static analysis) is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution. The term ...
* Temporal logic in finite-state verification * Post-silicon validation *
Intelligent verification {{Use American English, date = April 2019 Intelligent Verification, including intelligent testbench automation, is a form of functional verification of electronic hardware designs used to verify that a design conforms to specification before devic ...
* Runtime verification


References

{{Reflist Electronic circuit verification Formal methods Logic in computer science Theoretical computer science